p:FinProbSpace, n:, i:{0..n}, X:(Outcome). E(n;X@i) = weighted-sum(p;X)   

latex

Definitions

weighted-sum(p;F), <a, b>, , s = t, {x:A| B(x)} , {i..j}, x:A. B(x), #$n, t  T, , , b, A, b, , (i = j), x:AB(x), P  Q, x:A  B(x), P & Q, P  Q, Unit, left + right, Outcome, if b then t else f fi , False, A  B, i  j < k, , FinProbSpace, i  j , -n, n+m, n - m, a < b, Void, P  Q, Dec(P), True, Type, f(a), X@i, rv-shift(x;X), , E(n;F), x.A(x), T, cons-seq(x;s), {T}, SQType(T), s ~ t, RandomVariable(p;n), ||as||

Lemmas

length wf1, ws-constant, random-variable wf, weighted-sum wf2, squash wf, true wf, expectation wf, expectation-constant, rv-shift wf, rv-sample wf, le wf, decidable int equal, ge wf, nat properties, finite-prob-space wf, nat wf, p-outcome wf, rationals wf, int seg wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf